\begin{thebibliography}{99}

\bibitem{Andrews} % OK
P\/.B\/.~Andrews,
{\it An Introduction to Mathematical Logic
     and Type Theory: to Truth through Proof},
Computer Science and Applied Mathematics Series
(Academic Press, 1986).

\bibitem{Camilleri-et-al} % OK
A.J.\ Camilleri, T\/.F\/.\ Melham and M.J.C. Gordon,
`Hardware Verification using Higher-Order Logic',
in: {\it From HDL Descriptions to Guaranteed Correct \mbox{Circuit}
Designs: Proceedings of the IFIP WG 10.2 Working Conference, Grenoble,
September 1986}, edited by D.\ Borrione (North-Holland, 1987), pp.\ 43--67.

\bibitem{Church} % OK
A.\ Church,
`{}A Formulation of the Simple Theory of Types',
{\it Journal of Symbolic Logic} Vol.\ 5 (1940), pp.\ 56--68.

\bibitem{coquand} % OK
T{}.\ Coquand, `{}An Analysis of Girard's Paradox',
in: {\it Proceedings of the ACM Conference on
Logic in Computer Science\/}, Boston, June, 1986.

\bibitem{ml-handbook} % OK
G.\ Cousineau, M.\ Gordon, G.\ Huet, R.\ Milner,
L.\ Paulson and C.\ Wadsworth,
{\it The ML Handbook} ({\small INRIA}, 1986).

\bibitem{goguen} % OK
J.A.\ Goguen, J.W.\ Thatcher, and E.G.\ Wagner,
`{}An initial algebra \mbox{approach} to the specification,
correctness, and implementation of abstract data types',
in: {\it Current Trends in Programming Methodology\/}
edited by R.T{}.\ Yeh (Prentice-Hall, 1978)
Vol. {\sc iv}, pp 80--149.

\bibitem{HOL-paper} % OK
M.\ Gordon,
{\it HOL: A Machine Oriented Formulation of Higher-Order Logic},
Technical Report No.\ 68 (revised version),
(University of Cambridge Computer Laboratory, July 1985).

\bibitem{Why-HOL-paper} % OK
M.\ Gordon,
`Why higher-order Logic
is a good formalism for specifying and verifying hardware',
in: {\it Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh
      Workshop on VLSI\/}, edited by G.\ Milne and
P.A.\ Subrahmanyam (North-Holland, 1986), pp.\ 153--177.

\bibitem{Edinburgh-LCF} % OK
M.\ Gordon, R.\ Milner and C.P\/.\ Wadsworth,
{\it Edinburgh LCF: A Mechanised Logic of Computation},
Lecture Notes in Computer Science, Vol.\ 78,
(Springer-Verlag, 1979).

\bibitem{Hanna-Daeche} % OK
F{}.K.\ Hanna and N.\ Daeche,
`Specification and Verification Using Higher-Order Logic: A Case Study',
in: {\it Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh
      Workshop on VLSI\/}, edited by G.\ Milne and
P.A.\ Subrahmanyam (North-Holland, 1986), pp.\ 179--213.

\bibitem{jrh:thesis}
J.\ Harrison,
{\it Theorem-proving with the Real Numbers},
{\rm CPHC/BCS Distinguished Dissertations},
(Springer, 1998).

\bibitem{hurd-thesis}
Joe Hurd.
{\it Formal Verification of Probabilistic Algorithms},
{\rm PhD thesis, University of Cambridge, 2002}.

\bibitem{Leisenring} % OK
A.\ Leisenring,
{\it Mathematical Logic and Hilbert's $\epsilon$-Symbol\/},
{\rm University Mathematical Series},
(Macdonald \& Co.\ Ltd., London, 1969).

\bibitem{MW} % OK
Z.\ Manna and R.\ Waldinger,
{\it The Logical Basis for Computer Programming\/}
(Addison-Wesley, 1985).

\bibitem{Melham-banff} % OK
T{}.F{}.\ Melham, `{}Automating Recursive Type Definitions
in Higher Order Logic',
in: {\it Current Trends in Hardware Verification and
Automated Theorem Proving\/}, edited by G.\ Birtwistle
and P.A.\ Subrahmanyam
(Springer-Verlag, 1989), pp.\ 341--386.

\bibitem{sml} % OK
R.\ Milner, M.\ Tofte and R.\ Harper,
{\it The Definition of Standard ML\/},
(The MIT Press, 1990).

\bibitem{lcp-rewrite} % OK
L.\ Paulson,
`{}A Higher-Order Implementation of Rewriting',
{\it Science of Computer Programming}, Vol.\ 3, (1983), pp.\ 119--149.

\bibitem{new-LCF-man} % OK
 L.\ Paulson,
{\it Logic and Computation: Interactive Proof with Cambridge LCF},
Cambridge Tracts in Theoretical Computer Science 2
(Cambridge University Press, 1987).

\bibitem{slind-thesis}
Konrad Slind.
{\it Reasoning about Terminating Functional Programs},
{\rm PhD thesis, Technical University of Munich, 1999}.

\bibitem{Stefan}%
S.\ Soko\l owski, `{}A note on tactics in \LCF',
Technical Report CSR-140-83, Department of Computer Science,
(University of Edinburgh, 1983).


\bibitem{Z} % CHECK?
M.\ Spivey,
{\it The Z Notation}, (Prentice-Hall, 1989).

\bibitem{wong}
Wai Wong.
`Modelling bit vectors in {HOL}: The word library',
in: {\em Higher
  Order Logic Theorem Proving and its Applications, {HUG} '93}, edited
by Jeffrey~J. Joyce and Carl-Johan~H. Seger (volume 780 of
  {\em Lecture Notes in Computer Science}, Springer-Verlag, 1994),
  pp.~371--384.


\end{thebibliography}



%%% Local Variables:
%%% mode: latex
%%% TeX-master: "description"
%%% End:
